mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props up_time -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 5e-2 --width 5e-2 --relative-width --p0 --p1
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.
Peak memory usage: 54 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0
+ State space exploration
State size: 16 bytes
States: 5820
Transitions: 5820
Branches: 16788
Rate: 84348 states/s
Time: 0.1 s
+ Property up_time
Value: 472.26168182517654
Bounds: [454.97477551564975, 489.54858813470327]
Time: 9.6 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
Min. prob. 1 states: 5820
Time for min. prob. 1 states: 0.0 s
+ Essential states
Iterations: 1
Essential states: 2666
Transitions: 2666
Branches: 13634
Time: 0.0 s
+ Optimistic value iteration
Total iterations: 61134
Verif. attempts: 12
Verif. iterations: 20517
Final epsilon: 4.132842291174597E-06
Time: 9.5 s
Exported results to file "/out.txt".